Nuprl Lemma : tree_node_wf
4,23
postcript
pdf
E
,
T
:Type,
x
:(
T
T
). tree_node(
x
)
tree_con(
E
;
T
)
latex
Definitions
tree_con(
E
;
T
)
,
tree_node(
x
)
,
x
:
A
.
B
(
x
)
,
t
T
origin
E, T:Type, x:(T
T). tree_node(x) 
tree_con(E;T) E, T:Type, x:(TT). tree_node(x) tree_con(E;T) x:A. B(x) T